T:Type, R:(TTprop{i:l}), x,y:T.
(x rel_star(T; R) y)  ((z:T. ((x rel_star(T; R) z)  (z R y)))  (x = y)) 

latex

Definitions	x:A. B(x), prop{i:l}, P  Q, x f y, rel_star(T; R), P  Q, x:A. B(x), P  Q, P  Q, P  Q, t  T, , A  B, A, False, guard(T), A c B, T, True, rel_exp(T; R; n), Y, if b then t else f fi , (i = j), tt
Lemmas	nat wf, rel exp wf, rel exp iff, le wf, squash wf, true wf